a(v) sends [tg,   f(x, v)] on link l  
== with declarations 
== ds:x : A
== da:a : B  rcv(l,tg) : T
== a(v) sends [<tg,s,v. f(s(x),v)>] s v on link l 

latex

---

clarification:

x: A
a: B
rcv(l,tg) : T
a(v) sends [tg,   f(x, v)] on link l  
== with declarations 
== ds:x : A
== da:fpf-join(KindDeq;a : B;rcv(l,tg) : T)
== a(v) sends <tg,s,v. f(s(x),v)>.nil s v on link l 

latex

Definitions	with declarations ds:dsda:dak(v) sends f s v on link l, f  g, KindDeq, x : v, rcv(l,tg)
FDL editor aliases	ma-single-sends1